1. Field of the Invention
The present invention relates to techniques for verifying the correctness of an integrated circuit design, and in particular to accelerating coverage convergence using symbolic properties.
2. Related Art
Integrated circuit designs have increasingly higher complexity. This complexity makes determining the correctness of the design both difficult and resource intensive. To verify the correctness of a design, a verification tool typically applies stimuli to the design under verification (DUV). In general, many stimuli and simulation runs are needed to achieve a reasonable coverage of the behavior of the DUV. The simulation outputs of the DUV can be compared to expected outputs to determine whether the design is providing the desired functionality.
Coverage is a key metric that measures the quality and project completeness in the functional verification of the design. Types of coverage targets can be characterized as either functional coverage targets or code coverage targets. In a functional coverage target, a user wants some scenario to happen in the design. For example, the user wants signal A to have value X at the same time that signal B has value Y. In contrast, the code coverage target can include branch (if, case) statement, and line coverage. These types of coverage targets are well known and therefore not described in further detail.
Note that conventional simulations cannot generate such scenario information—hence the need for the user to specify coverage targets in a test bench. For example, FIG. 1 illustrates a conventional environment for a verification tool with an open loop, coverage convergence technique. In this environment, variables 101 of the hardware description language (HDL) code (typically in a register transfer level (RTL) format) of a design 103 are identified. In one embodiment, variables 101 are the input variables of design 103. In another embodiment, variables 101 are the input variables of specific starting points in design 103. After identification, randomized values 102 (i.e. stimuli) for variables 101 can be generated.
These randomized values 102 as well as user-provided coverage targets 104 can be provided to design 103 for simulation. In one embodiment, these simulations can be performed using a test bench 106 and design 103 is then typically referred to as a device-under-test (DUT). In another embodiment, the randomized values 102 can also be generated by test bench 106. The simulation results can be analyzed using functional verification and then provided to the user as coverage results 105.
Conventional functional verification uses constrained random simulation, which enables users to go from 0 to 80-90% coverage by automatically creating thousands of tests (i.e. different stimuli). However, getting the remaining 10-20% coverage is a very time consuming and difficult manual process. Typically, this process requires that verification engineers work with design engineers to analyze the coverage obtained so far, identify coverage holes, determine the reasons for not reaching the missing coverage targets, and write new tests to hit the missing targets and achieve coverage convergence. Unfortunately, this coverage convergence phase of verification can take up to 30% of the overall chip development cycle.
Previous techniques for automatically reaching the missing coverage targets have encountered severe scalability problems and require extensive modifications to existing verification tools. One such technique relies on randomly changing paths based on symbolic properties with the goal of executing new, previously un-explored branches in the code.
Therefore, a need arises for a coverage convergence technique that can automatically increase the number of reached coverage targets. This technique should scale to any size design and require minimal modifications to existing verification tools.